package tr.edu.ege.kipler.satisfiability.completion.rules.nondeterminism;

import java.util.ArrayList;
import java.util.HashSet;
import java.util.List;
import java.util.Set;

import tr.edu.ege.kipler.satisfiability.UnsatisfiableException;
import tr.edu.ege.kipler.satisfiability.container.World;
import tr.edu.ege.kipler.satisfiability.container.WorldConstraintSystem;
import tr.edu.ege.kipler.syntax.WorldElement;
import tr.edu.ege.kipler.syntax.atomicformula.Formula;

/**
 * 
 * @author İnanç Seylan
 *
 */
public class OrBranchingPoint extends BranchingPoint {

	private int index;

	private Set<WorldConstraintSystem> dependencySet = new HashSet<WorldConstraintSystem>();

	private Formula branchCause;

	private List<WorldElement> formulas = new ArrayList<WorldElement>();

	public Formula getBranchCause() {
		return branchCause;
	}

	public void setBranchCause(Formula branchCause) {
		this.branchCause = branchCause;
	}

	public boolean addFormula(WorldElement o) {
		return formulas.add(o);
	}

	protected List<WorldElement> getFormulas() {
		return formulas;
	}

	private Set<WorldConstraintSystem> getDependencySet() {
		return dependencySet;
	}

	@Override
	public boolean hasNext() {
		return index < getFormulas().size();
	}

	public WorldConstraintSystem next() throws UnsatisfiableException {
		WorldConstraintSystem result = null;
		if (index == 0) {
			WorldElement disjunct1 = getFormulas().get(index++);
			result = getWcs().copy();
			result.setId(getWcs().getId() + 1);
			World newWorld = result.getWorld(getWorld().getName());
			result.getData().getDependencyManager().add(disjunct1, getWcs());
			newWorld.add(disjunct1);
		} else if (index == 1) {
			getDependencySet().addAll(getLastBranchDependencies());
			getDependencySet().remove(getWcs());
			result = getWcs();
			World newWorld = result.getWorld(getWorld().getName());
			WorldElement negDisjunct1 = getFormulas().get(0).copy()
					.toggleNegated();
			result.getData().getDependencyManager().addAll(negDisjunct1,
					getDependencySet());
			newWorld.add(negDisjunct1);
			WorldElement disjunct2 = getFormulas().get(index++);
			result.getData().getDependencyManager().addAll(disjunct2,
					getDependencySet());
			result.getData().getDependencyManager().move(disjunct2,
					getBranchCause());
			newWorld.add(disjunct2);
		}
		return result;
	}
}
